
\section{Introduction}\label{sec:introduction}

Iterative development~\cite{Larman2003} is often adopted in modern
software projects~\cite{Schwaber2001} as it allows for rapid validation of the
developed features at a finer granularity. In Model-driven Engineering,
iterative modeling is often witnessed in model evolution~\cite{Meyers2011}. In
order to design a complete and correct model with respect to a set of
requirements, the development of the model is divided into several iterations. The
main issue with iterative modeling is that there is no guarantee that the model
$M_i$ resulting after an iteration $i$ does not break properties of the previous
model $M_{i-1}$ which correctly satisfied requirements. Therefore from a quality
assurance point of view, it is crucial that a model evolves (or increments)
correctly at each iteration.

The goal of this paper is to study how a behavioral model can safely evolve
without loosing the fact that a set of requirements were already satisfied in
its previous version. We use a specific formalization of the notions of
\emph{model} and \emph{requirement}. To express behavioral models, we chose a
fundamental, but usable, computing machine---algebraic Petri nets
(APN)~\cite{Rei91}---and CTL (Computational Tree
Logic)~\cite{Clarke86automaticverification} for expressing requirements for
those models.

In \Sect\ref{sec:operational_dref} we present the formal framework that
guarantees the quality criteria of property preservation. In
\Sect\ref{sec:motivation} we describe the confidential file system case study.
In \Sect\ref{sec:prop_preserv_evol} we demonstrate, by means of a concrete case
of iterative modeling, how each evolved model preserves the features from its
earlier version while adding new ones. \Sect\ref{sec:related_work} addresses the
applicability of the framework and related work. We conclude in
\Sect\ref{sec:conclusion}.
